Left Termination of the query pattern
delete(a,a,g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 876 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 460 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 30 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇒, 0 ms)
        ↳32 QDP
        ↳33 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES
    ↳35 PiDP
        ↳36 UsableRulesProof (⇔, 0 ms)
        ↳37 PiDP
        ↳38 PiDPToQDPProof (⇒, 0 ms)
        ↳39 QDP
        ↳40 QDPSizeChangeProof (⇔, 0 ms)
        ↳41 YES
    ↳42 PiDP
        ↳43 UsableRulesProof (⇔, 0 ms)
        ↳44 PiDP
        ↳45 PiDPToQDPProof (⇒, 0 ms)
        ↳46 QDP
        ↳47 QDPSizeChangeProof (⇔, 0 ms)
        ↳48 YES

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(a,a,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

delminA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delminA(X2, X4, X5).
lessB(s(X1), s(X2)) :- lessB(X1, X2).
deleteC(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delminA(X3, X4, X5).
deleteC(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- lessD(X1, X2).
deleteC(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscD(X1, X2), deleteC(X1, X3, X5)).
deleteC(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- lessD(X2, X1).
deleteC(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscD(X2, X1), deleteC(X1, X4, X5)).
lessD(s(X1), s(X2)) :- lessD(X1, X2).
lessJ(s(X1), s(X2)) :- lessJ(X1, X2).
pG(X1, X2, X3, X4) :- lessJ(X1, X2).
pG(X1, X2, X3, X4) :- ','(lesscJ(X1, X2), deleteE(X2, X3, X4)).
pF(X1, X2, X3, X4) :- lessB(X1, X2).
pF(X1, X2, X3, X4) :- ','(lesscB(X1, X2), deleteC(X1, X3, X4)).
pH(X1, X2, X3, X4) :- lessB(X1, X2).
pH(X1, X2, X3, X4) :- ','(lesscB(X1, X2), deleteC(s(X1), X3, X4)).
pI(X1, X2, X3, X4) :- lessJ(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscJ(X1, X2), deleteE(s(X2), X3, X4)).
deleteE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminA(X4, X6, X7).
deleteE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pF(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteC(0, X2, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteE(s(X1), X3, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- pI(X2, X1, X4, X5).
deleteE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminA(X4, X6, X7).
deleteE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pF(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteC(0, X2, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteE(s(X1), X3, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- pI(X2, X1, X4, X5).
deleteE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminA(X4, X6, X7).
deleteE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pF(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteC(0, X2, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteE(s(X1), X3, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- pI(X2, X1, X4, X5).
deleteE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminA(X4, X6, X7).
deleteE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pF(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteC(0, X2, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- pH(X1, X2, X3, X5).
deleteE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pG(X2, X1, X4, X5).
deleteE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteE(s(X1), X3, X4).
deleteE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- pI(X2, X1, X4, X5).

Clauses:

delmincA(tree(X1, void, X2), X1, X2).
delmincA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delmincA(X2, X4, X5).
lesscB(0, s(X1)).
lesscB(s(X1), s(X2)) :- lesscB(X1, X2).
deletecC(X1, tree(X1, void, X2), X2).
deletecC(X1, tree(X1, X2, void), X2).
deletecC(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delmincA(X3, X4, X5).
deletecC(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscD(X1, X2), deletecC(X1, X3, X5)).
deletecC(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- ','(lesscD(X2, X1), deletecC(X1, X4, X5)).
lesscD(0, s(X1)).
lesscD(s(X1), s(X2)) :- lesscD(X1, X2).
deletecE(X1, tree(X1, void, X2), X2).
deletecE(X1, tree(X1, X2, void), X2).
deletecE(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincA(X4, X6, X7).
deletecE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcF(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecC(0, X2, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecE(s(X1), X3, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- qcI(X2, X1, X4, X5).
deletecE(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincA(X4, X6, X7).
deletecE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcF(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecC(0, X2, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecE(s(X1), X3, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- qcI(X2, X1, X4, X5).
deletecE(X1, tree(X1, X2, void), X2).
deletecE(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincA(X4, X6, X7).
deletecE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcF(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecC(0, X2, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecE(s(X1), X3, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- qcI(X2, X1, X4, X5).
deletecE(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecE(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincA(X4, X6, X7).
deletecE(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcF(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecC(0, X2, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- qcH(X1, X2, X3, X5).
deletecE(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcG(X2, X1, X4, X5).
deletecE(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecE(s(X1), X3, X4).
deletecE(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- qcI(X2, X1, X4, X5).
lesscJ(0, s(X1)).
lesscJ(s(X1), s(X2)) :- lesscJ(X1, X2).
qcG(X1, X2, X3, X4) :- ','(lesscJ(X1, X2), deletecE(X2, X3, X4)).
qcF(X1, X2, X3, X4) :- ','(lesscB(X1, X2), deletecC(X1, X3, X4)).
qcH(X1, X2, X3, X4) :- ','(lesscB(X1, X2), deletecC(s(X1), X3, X4)).
qcI(X1, X2, X3, X4) :- ','(lesscJ(X1, X2), deletecE(s(X2), X3, X4)).

Afs:

deleteE(x1, x2, x3)  =  deleteE(x3)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
deleteE_in: (f,f,b)
delminA_in: (f,b,b)
pF_in: (f,b,f,b)
lessB_in: (f,b)
lesscB_in: (f,b)
deleteC_in: (b,f,b)
lessD_in: (b,b)
lesscD_in: (b,b)
pG_in: (b,f,f,b)
lessJ_in: (b,f)
lesscJ_in: (b,f)
pH_in: (f,b,f,b)
pI_in: (b,f,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETEE_IN_AAG(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U24_AAG(X1, X2, X3, X4, X5, X6, X7, X8, delminA_in_agg(X4, X6, X7))
DELETEE_IN_AAG(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMINA_IN_AGG(X4, X6, X7)
DELMINA_IN_AGG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U1_AGG(X1, X2, X3, X4, X5, X6, delminA_in_agg(X2, X4, X5))
DELMINA_IN_AGG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMINA_IN_AGG(X2, X4, X5)
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U25_AAG(X1, X2, X3, X4, X5, pF_in_agag(X1, X2, X3, X5))
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PF_IN_AGAG(X1, X2, X3, X5)
PF_IN_AGAG(X1, X2, X3, X4) → U15_AGAG(X1, X2, X3, X4, lessB_in_ag(X1, X2))
PF_IN_AGAG(X1, X2, X3, X4) → LESSB_IN_AG(X1, X2)
LESSB_IN_AG(s(X1), s(X2)) → U2_AG(X1, X2, lessB_in_ag(X1, X2))
LESSB_IN_AG(s(X1), s(X2)) → LESSB_IN_AG(X1, X2)
PF_IN_AGAG(X1, X2, X3, X4) → U16_AGAG(X1, X2, X3, X4, lesscB_in_ag(X1, X2))
U16_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → U17_AGAG(X1, X2, X3, X4, deleteC_in_gag(X1, X3, X4))
U16_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → DELETEC_IN_GAG(X1, X3, X4)
DELETEC_IN_GAG(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → U3_GAG(X1, X2, X3, X4, X5, delminA_in_agg(X3, X4, X5))
DELETEC_IN_GAG(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → DELMINA_IN_AGG(X3, X4, X5)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U4_GAG(X1, X2, X3, X4, X5, lessD_in_gg(X1, X2))
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → LESSD_IN_GG(X1, X2)
LESSD_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessD_in_gg(X1, X2))
LESSD_IN_GG(s(X1), s(X2)) → LESSD_IN_GG(X1, X2)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X1, X2))
U5_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → U6_GAG(X1, X2, X3, X4, X5, deleteC_in_gag(X1, X3, X5))
U5_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → DELETEC_IN_GAG(X1, X3, X5)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U7_GAG(X1, X2, X3, X4, X5, lessD_in_gg(X2, X1))
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSD_IN_GG(X2, X1)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X2, X1))
U8_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X2, X1)) → U9_GAG(X1, X2, X3, X4, X5, deleteC_in_gag(X1, X4, X5))
U8_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X2, X1)) → DELETEC_IN_GAG(X1, X4, X5)
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U26_AAG(X1, X2, X3, X4, X5, pG_in_gaag(X2, X1, X4, X5))
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PG_IN_GAAG(X2, X1, X4, X5)
PG_IN_GAAG(X1, X2, X3, X4) → U12_GAAG(X1, X2, X3, X4, lessJ_in_ga(X1, X2))
PG_IN_GAAG(X1, X2, X3, X4) → LESSJ_IN_GA(X1, X2)
LESSJ_IN_GA(s(X1), s(X2)) → U11_GA(X1, X2, lessJ_in_ga(X1, X2))
LESSJ_IN_GA(s(X1), s(X2)) → LESSJ_IN_GA(X1, X2)
PG_IN_GAAG(X1, X2, X3, X4) → U13_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U13_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → U14_GAAG(X1, X2, X3, X4, deleteE_in_aag(X2, X3, X4))
U13_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(X2, X3, X4)
DELETEE_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U27_AAG(X1, X2, X3, X4, deleteC_in_gag(0, X2, X4))
DELETEE_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEC_IN_GAG(0, X2, X4)
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U28_AAG(X1, X2, X3, X4, X5, pH_in_agag(X1, X2, X3, X5))
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → PH_IN_AGAG(X1, X2, X3, X5)
PH_IN_AGAG(X1, X2, X3, X4) → U18_AGAG(X1, X2, X3, X4, lessB_in_ag(X1, X2))
PH_IN_AGAG(X1, X2, X3, X4) → LESSB_IN_AG(X1, X2)
PH_IN_AGAG(X1, X2, X3, X4) → U19_AGAG(X1, X2, X3, X4, lesscB_in_ag(X1, X2))
U19_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → U20_AGAG(X1, X2, X3, X4, deleteC_in_gag(s(X1), X3, X4))
U19_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → DELETEC_IN_GAG(s(X1), X3, X4)
DELETEE_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U29_AAG(X1, X2, X3, X4, deleteE_in_aag(s(X1), X3, X4))
DELETEE_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEE_IN_AAG(s(X1), X3, X4)
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U30_AAG(X1, X2, X3, X4, X5, pI_in_gaag(X2, X1, X4, X5))
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U21_GAAG(X1, X2, X3, X4, lessJ_in_ga(X1, X2))
PI_IN_GAAG(X1, X2, X3, X4) → LESSJ_IN_GA(X1, X2)
PI_IN_GAAG(X1, X2, X3, X4) → U22_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U22_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → U23_GAAG(X1, X2, X3, X4, deleteE_in_aag(s(X2), X3, X4))
U22_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(s(X2), X3, X4)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
deleteE_in_aag(x1, x2, x3)  =  deleteE_in_aag(x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
pF_in_agag(x1, x2, x3, x4)  =  pF_in_agag(x2, x4)
lessB_in_ag(x1, x2)  =  lessB_in_ag(x2)
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
deleteC_in_gag(x1, x2, x3)  =  deleteC_in_gag(x1, x3)
lessD_in_gg(x1, x2)  =  lessD_in_gg(x1, x2)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
pG_in_gaag(x1, x2, x3, x4)  =  pG_in_gaag(x1, x4)
lessJ_in_ga(x1, x2)  =  lessJ_in_ga(x1)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
pH_in_agag(x1, x2, x3, x4)  =  pH_in_agag(x2, x4)
pI_in_gaag(x1, x2, x3, x4)  =  pI_in_gaag(x1, x4)
DELETEE_IN_AAG(x1, x2, x3)  =  DELETEE_IN_AAG(x3)
U24_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U24_AAG(x2, x3, x6, x7, x8, x9)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x1, x4, x5, x6, x7)
U25_AAG(x1, x2, x3, x4, x5, x6)  =  U25_AAG(x2, x4, x5, x6)
PF_IN_AGAG(x1, x2, x3, x4)  =  PF_IN_AGAG(x2, x4)
U15_AGAG(x1, x2, x3, x4, x5)  =  U15_AGAG(x2, x4, x5)
LESSB_IN_AG(x1, x2)  =  LESSB_IN_AG(x2)
U2_AG(x1, x2, x3)  =  U2_AG(x2, x3)
U16_AGAG(x1, x2, x3, x4, x5)  =  U16_AGAG(x2, x4, x5)
U17_AGAG(x1, x2, x3, x4, x5)  =  U17_AGAG(x1, x2, x4, x5)
DELETEC_IN_GAG(x1, x2, x3)  =  DELETEC_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5, x6)  =  U3_GAG(x1, x2, x4, x5, x6)
U4_GAG(x1, x2, x3, x4, x5, x6)  =  U4_GAG(x1, x2, x4, x5, x6)
LESSD_IN_GG(x1, x2)  =  LESSD_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U5_GAG(x1, x2, x3, x4, x5, x6)  =  U5_GAG(x1, x2, x4, x5, x6)
U6_GAG(x1, x2, x3, x4, x5, x6)  =  U6_GAG(x1, x2, x4, x5, x6)
U7_GAG(x1, x2, x3, x4, x5, x6)  =  U7_GAG(x1, x2, x3, x5, x6)
U8_GAG(x1, x2, x3, x4, x5, x6)  =  U8_GAG(x1, x2, x3, x5, x6)
U9_GAG(x1, x2, x3, x4, x5, x6)  =  U9_GAG(x1, x2, x3, x5, x6)
U26_AAG(x1, x2, x3, x4, x5, x6)  =  U26_AAG(x2, x3, x5, x6)
PG_IN_GAAG(x1, x2, x3, x4)  =  PG_IN_GAAG(x1, x4)
U12_GAAG(x1, x2, x3, x4, x5)  =  U12_GAAG(x1, x4, x5)
LESSJ_IN_GA(x1, x2)  =  LESSJ_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U13_GAAG(x1, x2, x3, x4, x5)  =  U13_GAAG(x1, x4, x5)
U14_GAAG(x1, x2, x3, x4, x5)  =  U14_GAAG(x1, x4, x5)
U27_AAG(x1, x2, x3, x4, x5)  =  U27_AAG(x1, x3, x4, x5)
U28_AAG(x1, x2, x3, x4, x5, x6)  =  U28_AAG(x2, x4, x5, x6)
PH_IN_AGAG(x1, x2, x3, x4)  =  PH_IN_AGAG(x2, x4)
U18_AGAG(x1, x2, x3, x4, x5)  =  U18_AGAG(x2, x4, x5)
U19_AGAG(x1, x2, x3, x4, x5)  =  U19_AGAG(x2, x4, x5)
U20_AGAG(x1, x2, x3, x4, x5)  =  U20_AGAG(x1, x2, x4, x5)
U29_AAG(x1, x2, x3, x4, x5)  =  U29_AAG(x2, x4, x5)
U30_AAG(x1, x2, x3, x4, x5, x6)  =  U30_AAG(x2, x3, x5, x6)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U21_GAAG(x1, x2, x3, x4, x5)  =  U21_GAAG(x1, x4, x5)
U22_GAAG(x1, x2, x3, x4, x5)  =  U22_GAAG(x1, x4, x5)
U23_GAAG(x1, x2, x3, x4, x5)  =  U23_GAAG(x1, x4, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEE_IN_AAG(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U24_AAG(X1, X2, X3, X4, X5, X6, X7, X8, delminA_in_agg(X4, X6, X7))
DELETEE_IN_AAG(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMINA_IN_AGG(X4, X6, X7)
DELMINA_IN_AGG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U1_AGG(X1, X2, X3, X4, X5, X6, delminA_in_agg(X2, X4, X5))
DELMINA_IN_AGG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMINA_IN_AGG(X2, X4, X5)
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U25_AAG(X1, X2, X3, X4, X5, pF_in_agag(X1, X2, X3, X5))
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PF_IN_AGAG(X1, X2, X3, X5)
PF_IN_AGAG(X1, X2, X3, X4) → U15_AGAG(X1, X2, X3, X4, lessB_in_ag(X1, X2))
PF_IN_AGAG(X1, X2, X3, X4) → LESSB_IN_AG(X1, X2)
LESSB_IN_AG(s(X1), s(X2)) → U2_AG(X1, X2, lessB_in_ag(X1, X2))
LESSB_IN_AG(s(X1), s(X2)) → LESSB_IN_AG(X1, X2)
PF_IN_AGAG(X1, X2, X3, X4) → U16_AGAG(X1, X2, X3, X4, lesscB_in_ag(X1, X2))
U16_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → U17_AGAG(X1, X2, X3, X4, deleteC_in_gag(X1, X3, X4))
U16_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → DELETEC_IN_GAG(X1, X3, X4)
DELETEC_IN_GAG(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → U3_GAG(X1, X2, X3, X4, X5, delminA_in_agg(X3, X4, X5))
DELETEC_IN_GAG(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → DELMINA_IN_AGG(X3, X4, X5)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U4_GAG(X1, X2, X3, X4, X5, lessD_in_gg(X1, X2))
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → LESSD_IN_GG(X1, X2)
LESSD_IN_GG(s(X1), s(X2)) → U10_GG(X1, X2, lessD_in_gg(X1, X2))
LESSD_IN_GG(s(X1), s(X2)) → LESSD_IN_GG(X1, X2)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X1, X2))
U5_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → U6_GAG(X1, X2, X3, X4, X5, deleteC_in_gag(X1, X3, X5))
U5_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → DELETEC_IN_GAG(X1, X3, X5)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U7_GAG(X1, X2, X3, X4, X5, lessD_in_gg(X2, X1))
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → LESSD_IN_GG(X2, X1)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X2, X1))
U8_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X2, X1)) → U9_GAG(X1, X2, X3, X4, X5, deleteC_in_gag(X1, X4, X5))
U8_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X2, X1)) → DELETEC_IN_GAG(X1, X4, X5)
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U26_AAG(X1, X2, X3, X4, X5, pG_in_gaag(X2, X1, X4, X5))
DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PG_IN_GAAG(X2, X1, X4, X5)
PG_IN_GAAG(X1, X2, X3, X4) → U12_GAAG(X1, X2, X3, X4, lessJ_in_ga(X1, X2))
PG_IN_GAAG(X1, X2, X3, X4) → LESSJ_IN_GA(X1, X2)
LESSJ_IN_GA(s(X1), s(X2)) → U11_GA(X1, X2, lessJ_in_ga(X1, X2))
LESSJ_IN_GA(s(X1), s(X2)) → LESSJ_IN_GA(X1, X2)
PG_IN_GAAG(X1, X2, X3, X4) → U13_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U13_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → U14_GAAG(X1, X2, X3, X4, deleteE_in_aag(X2, X3, X4))
U13_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(X2, X3, X4)
DELETEE_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U27_AAG(X1, X2, X3, X4, deleteC_in_gag(0, X2, X4))
DELETEE_IN_AAG(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEC_IN_GAG(0, X2, X4)
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U28_AAG(X1, X2, X3, X4, X5, pH_in_agag(X1, X2, X3, X5))
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → PH_IN_AGAG(X1, X2, X3, X5)
PH_IN_AGAG(X1, X2, X3, X4) → U18_AGAG(X1, X2, X3, X4, lessB_in_ag(X1, X2))
PH_IN_AGAG(X1, X2, X3, X4) → LESSB_IN_AG(X1, X2)
PH_IN_AGAG(X1, X2, X3, X4) → U19_AGAG(X1, X2, X3, X4, lesscB_in_ag(X1, X2))
U19_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → U20_AGAG(X1, X2, X3, X4, deleteC_in_gag(s(X1), X3, X4))
U19_AGAG(X1, X2, X3, X4, lesscB_out_ag(X1, X2)) → DELETEC_IN_GAG(s(X1), X3, X4)
DELETEE_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U29_AAG(X1, X2, X3, X4, deleteE_in_aag(s(X1), X3, X4))
DELETEE_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEE_IN_AAG(s(X1), X3, X4)
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U30_AAG(X1, X2, X3, X4, X5, pI_in_gaag(X2, X1, X4, X5))
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U21_GAAG(X1, X2, X3, X4, lessJ_in_ga(X1, X2))
PI_IN_GAAG(X1, X2, X3, X4) → LESSJ_IN_GA(X1, X2)
PI_IN_GAAG(X1, X2, X3, X4) → U22_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U22_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → U23_GAAG(X1, X2, X3, X4, deleteE_in_aag(s(X2), X3, X4))
U22_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(s(X2), X3, X4)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
deleteE_in_aag(x1, x2, x3)  =  deleteE_in_aag(x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
delminA_in_agg(x1, x2, x3)  =  delminA_in_agg(x2, x3)
pF_in_agag(x1, x2, x3, x4)  =  pF_in_agag(x2, x4)
lessB_in_ag(x1, x2)  =  lessB_in_ag(x2)
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
deleteC_in_gag(x1, x2, x3)  =  deleteC_in_gag(x1, x3)
lessD_in_gg(x1, x2)  =  lessD_in_gg(x1, x2)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
pG_in_gaag(x1, x2, x3, x4)  =  pG_in_gaag(x1, x4)
lessJ_in_ga(x1, x2)  =  lessJ_in_ga(x1)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
pH_in_agag(x1, x2, x3, x4)  =  pH_in_agag(x2, x4)
pI_in_gaag(x1, x2, x3, x4)  =  pI_in_gaag(x1, x4)
DELETEE_IN_AAG(x1, x2, x3)  =  DELETEE_IN_AAG(x3)
U24_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U24_AAG(x2, x3, x6, x7, x8, x9)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x1, x4, x5, x6, x7)
U25_AAG(x1, x2, x3, x4, x5, x6)  =  U25_AAG(x2, x4, x5, x6)
PF_IN_AGAG(x1, x2, x3, x4)  =  PF_IN_AGAG(x2, x4)
U15_AGAG(x1, x2, x3, x4, x5)  =  U15_AGAG(x2, x4, x5)
LESSB_IN_AG(x1, x2)  =  LESSB_IN_AG(x2)
U2_AG(x1, x2, x3)  =  U2_AG(x2, x3)
U16_AGAG(x1, x2, x3, x4, x5)  =  U16_AGAG(x2, x4, x5)
U17_AGAG(x1, x2, x3, x4, x5)  =  U17_AGAG(x1, x2, x4, x5)
DELETEC_IN_GAG(x1, x2, x3)  =  DELETEC_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5, x6)  =  U3_GAG(x1, x2, x4, x5, x6)
U4_GAG(x1, x2, x3, x4, x5, x6)  =  U4_GAG(x1, x2, x4, x5, x6)
LESSD_IN_GG(x1, x2)  =  LESSD_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x1, x2, x3)
U5_GAG(x1, x2, x3, x4, x5, x6)  =  U5_GAG(x1, x2, x4, x5, x6)
U6_GAG(x1, x2, x3, x4, x5, x6)  =  U6_GAG(x1, x2, x4, x5, x6)
U7_GAG(x1, x2, x3, x4, x5, x6)  =  U7_GAG(x1, x2, x3, x5, x6)
U8_GAG(x1, x2, x3, x4, x5, x6)  =  U8_GAG(x1, x2, x3, x5, x6)
U9_GAG(x1, x2, x3, x4, x5, x6)  =  U9_GAG(x1, x2, x3, x5, x6)
U26_AAG(x1, x2, x3, x4, x5, x6)  =  U26_AAG(x2, x3, x5, x6)
PG_IN_GAAG(x1, x2, x3, x4)  =  PG_IN_GAAG(x1, x4)
U12_GAAG(x1, x2, x3, x4, x5)  =  U12_GAAG(x1, x4, x5)
LESSJ_IN_GA(x1, x2)  =  LESSJ_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
U13_GAAG(x1, x2, x3, x4, x5)  =  U13_GAAG(x1, x4, x5)
U14_GAAG(x1, x2, x3, x4, x5)  =  U14_GAAG(x1, x4, x5)
U27_AAG(x1, x2, x3, x4, x5)  =  U27_AAG(x1, x3, x4, x5)
U28_AAG(x1, x2, x3, x4, x5, x6)  =  U28_AAG(x2, x4, x5, x6)
PH_IN_AGAG(x1, x2, x3, x4)  =  PH_IN_AGAG(x2, x4)
U18_AGAG(x1, x2, x3, x4, x5)  =  U18_AGAG(x2, x4, x5)
U19_AGAG(x1, x2, x3, x4, x5)  =  U19_AGAG(x2, x4, x5)
U20_AGAG(x1, x2, x3, x4, x5)  =  U20_AGAG(x1, x2, x4, x5)
U29_AAG(x1, x2, x3, x4, x5)  =  U29_AAG(x2, x4, x5)
U30_AAG(x1, x2, x3, x4, x5, x6)  =  U30_AAG(x2, x3, x5, x6)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U21_GAAG(x1, x2, x3, x4, x5)  =  U21_GAAG(x1, x4, x5)
U22_GAAG(x1, x2, x3, x4, x5)  =  U22_GAAG(x1, x4, x5)
U23_GAAG(x1, x2, x3, x4, x5)  =  U23_GAAG(x1, x4, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 39 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSJ_IN_GA(s(X1), s(X2)) → LESSJ_IN_GA(X1, X2)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
LESSJ_IN_GA(x1, x2)  =  LESSJ_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSJ_IN_GA(s(X1), s(X2)) → LESSJ_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSJ_IN_GA(x1, x2)  =  LESSJ_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSJ_IN_GA(s(X1)) → LESSJ_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSJ_IN_GA(s(X1)) → LESSJ_IN_GA(X1)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSD_IN_GG(s(X1), s(X2)) → LESSD_IN_GG(X1, X2)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
LESSD_IN_GG(x1, x2)  =  LESSD_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSD_IN_GG(s(X1), s(X2)) → LESSD_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSD_IN_GG(s(X1), s(X2)) → LESSD_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSD_IN_GG(s(X1), s(X2)) → LESSD_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSB_IN_AG(s(X1), s(X2)) → LESSB_IN_AG(X1, X2)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
LESSB_IN_AG(x1, x2)  =  LESSB_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSB_IN_AG(s(X1), s(X2)) → LESSB_IN_AG(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSB_IN_AG(x1, x2)  =  LESSB_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSB_IN_AG(s(X2)) → LESSB_IN_AG(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSB_IN_AG(s(X2)) → LESSB_IN_AG(X2)
    The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMINA_IN_AGG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMINA_IN_AGG(X2, X4, X5)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMINA_IN_AGG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMINA_IN_AGG(X2, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
DELMINA_IN_AGG(x1, x2, x3)  =  DELMINA_IN_AGG(x2, x3)

We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELMINA_IN_AGG(X4, tree(X1, X5, X6)) → DELMINA_IN_AGG(X4, X5)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELMINA_IN_AGG(X4, tree(X1, X5, X6)) → DELMINA_IN_AGG(X4, X5)
    The graph contains the following edges 1 >= 1, 2 > 2

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X1, X2))
U5_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → DELETEC_IN_GAG(X1, X3, X5)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X2, X1))
U8_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X2, X1)) → DELETEC_IN_GAG(X1, X4, X5)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
DELETEC_IN_GAG(x1, x2, x3)  =  DELETEC_IN_GAG(x1, x3)
U5_GAG(x1, x2, x3, x4, x5, x6)  =  U5_GAG(x1, x2, x4, x5, x6)
U8_GAG(x1, x2, x3, x4, x5, x6)  =  U8_GAG(x1, x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U5_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X1, X2))
U5_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X1, X2)) → DELETEC_IN_GAG(X1, X3, X5)
DELETEC_IN_GAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U8_GAG(X1, X2, X3, X4, X5, lesscD_in_gg(X2, X1))
U8_GAG(X1, X2, X3, X4, X5, lesscD_out_gg(X2, X1)) → DELETEC_IN_GAG(X1, X4, X5)

The TRS R consists of the following rules:

lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
DELETEC_IN_GAG(x1, x2, x3)  =  DELETEC_IN_GAG(x1, x3)
U5_GAG(x1, x2, x3, x4, x5, x6)  =  U5_GAG(x1, x2, x4, x5, x6)
U8_GAG(x1, x2, x3, x4, x5, x6)  =  U8_GAG(x1, x2, x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETEC_IN_GAG(X1, tree(X2, X5, X4)) → U5_GAG(X1, X2, X4, X5, lesscD_in_gg(X1, X2))
U5_GAG(X1, X2, X4, X5, lesscD_out_gg(X1, X2)) → DELETEC_IN_GAG(X1, X5)
DELETEC_IN_GAG(X1, tree(X2, X3, X5)) → U8_GAG(X1, X2, X3, X5, lesscD_in_gg(X2, X1))
U8_GAG(X1, X2, X3, X5, lesscD_out_gg(X2, X1)) → DELETEC_IN_GAG(X1, X5)

The TRS R consists of the following rules:

lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lesscD_in_gg(x0, x1)
U39_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U5_GAG(X1, X2, X4, X5, lesscD_out_gg(X1, X2)) → DELETEC_IN_GAG(X1, X5)
    The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2

  • U8_GAG(X1, X2, X3, X5, lesscD_out_gg(X2, X1)) → DELETEC_IN_GAG(X1, X5)
    The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2

  • DELETEC_IN_GAG(X1, tree(X2, X5, X4)) → U5_GAG(X1, X2, X4, X5, lesscD_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

  • DELETEC_IN_GAG(X1, tree(X2, X3, X5)) → U8_GAG(X1, X2, X3, X5, lesscD_in_gg(X2, X1))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PG_IN_GAAG(X2, X1, X4, X5)
PG_IN_GAAG(X1, X2, X3, X4) → U13_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U13_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(X2, X3, X4)
DELETEE_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEE_IN_AAG(s(X1), X3, X4)
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U22_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U22_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(s(X2), X3, X4)

The TRS R consists of the following rules:

lesscB_in_ag(0, s(X1)) → lesscB_out_ag(0, s(X1))
lesscB_in_ag(s(X1), s(X2)) → U33_ag(X1, X2, lesscB_in_ag(X1, X2))
U33_ag(X1, X2, lesscB_out_ag(X1, X2)) → lesscB_out_ag(s(X1), s(X2))
lesscD_in_gg(0, s(X1)) → lesscD_out_gg(0, s(X1))
lesscD_in_gg(s(X1), s(X2)) → U39_gg(X1, X2, lesscD_in_gg(X1, X2))
U39_gg(X1, X2, lesscD_out_gg(X1, X2)) → lesscD_out_gg(s(X1), s(X2))
lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscB_in_ag(x1, x2)  =  lesscB_in_ag(x2)
lesscB_out_ag(x1, x2)  =  lesscB_out_ag(x1, x2)
U33_ag(x1, x2, x3)  =  U33_ag(x2, x3)
lesscD_in_gg(x1, x2)  =  lesscD_in_gg(x1, x2)
0  =  0
lesscD_out_gg(x1, x2)  =  lesscD_out_gg(x1, x2)
U39_gg(x1, x2, x3)  =  U39_gg(x1, x2, x3)
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
DELETEE_IN_AAG(x1, x2, x3)  =  DELETEE_IN_AAG(x3)
PG_IN_GAAG(x1, x2, x3, x4)  =  PG_IN_GAAG(x1, x4)
U13_GAAG(x1, x2, x3, x4, x5)  =  U13_GAAG(x1, x4, x5)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U22_GAAG(x1, x2, x3, x4, x5)  =  U22_GAAG(x1, x4, x5)

We have to consider all (P,R,Pi)-chains

(43) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEE_IN_AAG(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PG_IN_GAAG(X2, X1, X4, X5)
PG_IN_GAAG(X1, X2, X3, X4) → U13_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U13_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(X2, X3, X4)
DELETEE_IN_AAG(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEE_IN_AAG(s(X1), X3, X4)
DELETEE_IN_AAG(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → PI_IN_GAAG(X2, X1, X4, X5)
PI_IN_GAAG(X1, X2, X3, X4) → U22_GAAG(X1, X2, X3, X4, lesscJ_in_ga(X1, X2))
U22_GAAG(X1, X2, X3, X4, lesscJ_out_ga(X1, X2)) → DELETEE_IN_AAG(s(X2), X3, X4)

The TRS R consists of the following rules:

lesscJ_in_ga(0, s(X1)) → lesscJ_out_ga(0, s(X1))
lesscJ_in_ga(s(X1), s(X2)) → U47_ga(X1, X2, lesscJ_in_ga(X1, X2))
U47_ga(X1, X2, lesscJ_out_ga(X1, X2)) → lesscJ_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lesscJ_in_ga(x1, x2)  =  lesscJ_in_ga(x1)
lesscJ_out_ga(x1, x2)  =  lesscJ_out_ga(x1)
U47_ga(x1, x2, x3)  =  U47_ga(x1, x3)
DELETEE_IN_AAG(x1, x2, x3)  =  DELETEE_IN_AAG(x3)
PG_IN_GAAG(x1, x2, x3, x4)  =  PG_IN_GAAG(x1, x4)
U13_GAAG(x1, x2, x3, x4, x5)  =  U13_GAAG(x1, x4, x5)
PI_IN_GAAG(x1, x2, x3, x4)  =  PI_IN_GAAG(x1, x4)
U22_GAAG(x1, x2, x3, x4, x5)  =  U22_GAAG(x1, x4, x5)

We have to consider all (P,R,Pi)-chains

(45) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETEE_IN_AAG(tree(X2, X3, X5)) → PG_IN_GAAG(X2, X5)
PG_IN_GAAG(X1, X4) → U13_GAAG(X1, X4, lesscJ_in_ga(X1))
U13_GAAG(X1, X4, lesscJ_out_ga(X1)) → DELETEE_IN_AAG(X4)
DELETEE_IN_AAG(tree(0, X2, X4)) → DELETEE_IN_AAG(X4)
DELETEE_IN_AAG(tree(s(X2), X3, X5)) → PI_IN_GAAG(X2, X5)
PI_IN_GAAG(X1, X4) → U22_GAAG(X1, X4, lesscJ_in_ga(X1))
U22_GAAG(X1, X4, lesscJ_out_ga(X1)) → DELETEE_IN_AAG(X4)

The TRS R consists of the following rules:

lesscJ_in_ga(0) → lesscJ_out_ga(0)
lesscJ_in_ga(s(X1)) → U47_ga(X1, lesscJ_in_ga(X1))
U47_ga(X1, lesscJ_out_ga(X1)) → lesscJ_out_ga(s(X1))

The set Q consists of the following terms:

lesscJ_in_ga(x0)
U47_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(47) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PG_IN_GAAG(X1, X4) → U13_GAAG(X1, X4, lesscJ_in_ga(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U13_GAAG(X1, X4, lesscJ_out_ga(X1)) → DELETEE_IN_AAG(X4)
    The graph contains the following edges 2 >= 1

  • DELETEE_IN_AAG(tree(X2, X3, X5)) → PG_IN_GAAG(X2, X5)
    The graph contains the following edges 1 > 1, 1 > 2

  • DELETEE_IN_AAG(tree(0, X2, X4)) → DELETEE_IN_AAG(X4)
    The graph contains the following edges 1 > 1

  • U22_GAAG(X1, X4, lesscJ_out_ga(X1)) → DELETEE_IN_AAG(X4)
    The graph contains the following edges 2 >= 1

  • DELETEE_IN_AAG(tree(s(X2), X3, X5)) → PI_IN_GAAG(X2, X5)
    The graph contains the following edges 1 > 1, 1 > 2

  • PI_IN_GAAG(X1, X4) → U22_GAAG(X1, X4, lesscJ_in_ga(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2

(48) YES